the_es:ES, l:IdLnk, e:{e:E| haslnk(l;e) }. emsg(e)  (Msg on l) 

latex

Definitions	Msg(M), mlnk(m), Prop, Msg, E, b, haslnk(l;e), IdLnk, ES, P  Q, P & Q, A & B, (Msg on l), emsg(e), x:A. B(x), P  Q, t  T, haslink(l;m)
Lemmas	es-msg wf, assert-es-haslnk, event system wf, IdLnk wf, es-haslnk wf, assert wf, es-E wf